Skip to content

feat: new, extensible do elaborator#12459

Merged
sgraf812 merged 27 commits intomasterfrom
sg/newdo
Feb 21, 2026
Merged

feat: new, extensible do elaborator#12459
sgraf812 merged 27 commits intomasterfrom
sg/newdo

Conversation

@sgraf812
Copy link
Contributor

@sgraf812 sgraf812 commented Feb 12, 2026 •
edited
Loading

This PR adds a new, extensible do elaborator. Users can opt into the new elaborator by unsetting the option backward.do.legacy.

New elaborators for the builtin doElem syntax category can be registered with attribute doElem_elab. For new syntax, additionally a control info handler must be registered with attribute doElem_control_info that specifies whether the new syntax returns early, breaks, continues and which mut vars it reassigns.

Do elaborators have type TSyntax `doElem → DoElemCont → DoElabM Expr, where DoElabM is essentially TermElabM and the DoElemCont represents how the rest of the do block is to be elaborated. Consult the docstrings for more details.

Breaking Changes:

  • The syntax for let pat := rhs | otherwise and similar now scope over the doSeq that follows. Furthermore, otherwise and the sequence that follows are now doSeqIndented in order not to steal syntax from record syntax.

Breaking Changes when opting into the new do elaborator by unsetting backward.do.legacy:

  • do notation now always requires Pure.
  • do match is now always non-dependent. There is do match (dependent := true) that expands to a
    term match as a workaround for some dependent uses.

@sgraf812 sgraf812 added the changelog-language Language features and metaprograms label Feb 12, 2026
@sgraf812 sgraf812 force-pushed the sg/newdo branch 3 times, most recently from 7f7e326 to 5a408a0 Compare February 12, 2026 17:15
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Feb 12, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 12, 2026 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 818a0ec6a74d6b9db984e197a1a959e5c540b682 --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-12 18:28:07)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 10770eda3e24cdc7a633079093de5344acfad17b --onto 309f44d00757482e1c5a2b2427fdca818a24615a. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-20 10:39:20)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Feb 12, 2026 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 818a0ec6a74d6b9db984e197a1a959e5c540b682 --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-12 18:28:10)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 10770eda3e24cdc7a633079093de5344acfad17b --onto 5c7a508e21c5ebc710b0dfe65648d5beba4e34e0. You can force reference manual CI using the force-manual-ci label. (2026-02-20 10:39:22)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-20 19:00:46)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-21 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-21 13:45:38)

@sgraf812
Copy link
Contributor Author

sgraf812 commented Feb 20, 2026

!bench

@sgraf812 sgraf812 marked this pull request as ready for review February 20, 2026 09:46
@leanprover-radar
Copy link

leanprover-radar commented Feb 20, 2026 •
edited
Loading

Benchmark results for f1132ca against 10770ed are in! @sgraf812

  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

No significant changes detected.

@sgraf812
Copy link
Contributor Author

sgraf812 commented Feb 20, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Feb 20, 2026 •
edited
Loading

Benchmark results for b3c96c5 against 10770ed are in! @sgraf812

  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

No significant changes detected.

@sgraf812
Copy link
Contributor Author

sgraf812 commented Feb 20, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Feb 20, 2026 •
edited
Loading

Benchmark results for 111f4d6 against 10770ed are in! @sgraf812

  • 🟥 build//instructions: +98.7G (+0.79%)

Large changes (5🟥)

  • 🟥 size/all/.ir//bytes: +3MiB (+0.89%)
  • 🟥 size/all/.olean.private//bytes: +9MiB (+0.76%)
  • 🟥 size/install//bytes: +17MiB (+0.70%)
  • 🟥 size/libleanshared.so//bytes: +1MiB (+0.91%)
  • 🟥 tests/compiler//sum binary sizes: +14.9M (+1.18%)

Medium changes (1✅)

  • ✅ build/module/Lean.Elab.Do.Switch//bytes .olean.private: -55kiB (-32.84%)

Small changes (2✅, 68🟥)

Too many entries to display here. View the full report on radar instead.

@github-actions github-actions bot added the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 20, 2026
@sgraf812
Copy link
Contributor Author

sgraf812 commented Feb 20, 2026 •
edited
Loading

Note that the new do elaborator is not active and the benchmark measures just the addition of new code. I think the benchmark results are acceptable. I suspect the bulk of it is due to addition of an attribute.

@github-actions github-actions bot removed the changes-stage0 Contains stage0 changes, merge manually using rebase label Feb 20, 2026
@sgraf812 sgraf812 force-pushed the sg/newdo branch 2 times, most recently from e12acef to 581b7a4 Compare February 20, 2026 17:56
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 20, 2026
Update lean-toolchain for testing leanprover/lean4#12459
ac8473a
@github-actions github-actions bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Feb 20, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 20, 2026
Update lean-toolchain for testing leanprover/lean4#12459
080ecd8
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Feb 20, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 21, 2026
Update lean-toolchain for leanprover/lean4#12459
4259e21
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 21, 2026
Update lean-toolchain for leanprover/lean4#12459
f3aa68c
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 21, 2026

Mathlib CI status (docs):

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 21, 2026
Update lean-toolchain for leanprover/lean4#12459
c639ea6
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 21, 2026
Update lean-toolchain for leanprover/lean4#12459
9ea4943
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Feb 21, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Feb 21, 2026

Mathlib CI status (docs):

@sgraf812 sgraf812 added this pull request to the merge queue Feb 21, 2026
Merged via the queue into master with commit 4278038 Feb 21, 2026
28 checks passed
@sgraf812 sgraf812 deleted the sg/newdo branch February 21, 2026 17:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@kmill kmill Awaiting requested review from kmill kmill is a code owner

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@sgraf812 @leanprover-bot @leanprover-radar